T:Type, L:(T List), R:({x:T| (x  L)} es_realizer{i:l}), es:event_system{i:l}.
R-consistent(Rall(L; x.R(x)); es)  l_all(L; T; x.R-consistent(R(x); es)) 

latex

Definitions	guard(T), P  Q, x. t(x), False, A, x:A. B(x), ff, tt, i <z j, b, i z j, if b then t else f fi , nth_tl(n;as), hd(l), A  B, lelt(i; j; k), ||as||, int_seg(i; j), l[i], A c B, (x  l), True, prop{i:l}, P  Q, P  Q, reduce(f; k; as), Y, P  Q, map(f; as), Rlist(L), l_all(L; T; x.P(x)), x(s), Rall(L; x.R(x)), R-consistent(R; es), P  Q, t  T, x:A. B(x),
Lemmas	and functionality wrt iff, l all wf2, cons member, Rall wf, select wf, nat wf, non neg length, length wf1, select member, iff functionality wrt iff, nil member, es realizer wf, event system wf, Rnone wf, R-consistent wf, l member wf